Search Results

Documents authored by Ohlmann, Pierre

Document
DOI: 10.4230/LIPIcs.STACS.2024.54
Positionality in Σ⁰₂ and a Completeness Result

Authors: Pierre Ohlmann and Michał Skrzypczak

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study the existence of positional strategies for the protagonist in infinite duration games over arbitrary game graphs. We prove that prefix-independent objectives in Σ⁰₂ which are positional and admit a (strongly) neutral letter are exactly those that are recognised by history-deterministic monotone co-Büchi automata over countable ordinals. This generalises a criterion proposed by [Kopczyński, ICALP 2006] and gives an alternative proof of closure under union for these objectives, which was known from [Ohlmann, TheoretiCS 2023]. We then give two applications of our result. First, we prove that the mean-payoff objective is positional over arbitrary game graphs. Second, we establish the following completeness result: for any objective W which is prefix-independent, admits a (weakly) neutral letter, and is positional over finite game graphs, there is an objective W' which is equivalent to W over finite game graphs and positional over arbitrary game graphs.
Cite as

Pierre Ohlmann and Michał Skrzypczak. Positionality in Σ⁰₂ and a Completeness Result. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 54:1-54:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ohlmann_et_al:LIPIcs.STACS.2024.54,
  author =	{Ohlmann, Pierre and Skrzypczak, Micha{\l}},
  title =	{{Positionality in \Sigma⁰₂ and a Completeness Result}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{54:1--54:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.54},
  URN =		{urn:nbn:de:0030-drops-197643},
  doi =		{10.4230/LIPIcs.STACS.2024.54},
  annote =	{Keywords: infinite duration games, positionality, Borel class \Sigma⁰₂, history determinism}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.122
Characterising Memory in Infinite Games

Authors: Antonio Casares and Pierre Ohlmann

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
This paper is concerned with games of infinite duration played over potentially infinite graphs. Recently, Ohlmann (TheoretiCS 2023) presented a characterisation of objectives admitting optimal positional strategies, by means of universal graphs: an objective is positional if and only if it admits well-ordered monotone universal graphs. We extend Ohlmann’s characterisation to encompass (finite or infinite) memory upper bounds. We prove that objectives admitting optimal strategies with ε-memory less than m (a memory that cannot be updated when reading an ε-edge) are exactly those which admit well-founded monotone universal graphs whose antichains have size bounded by m. We also give a characterisation of chromatic memory by means of appropriate universal structures. Our results apply to finite as well as infinite memory bounds (for instance, to objectives with finite but unbounded memory, or with countable memory strategies). We illustrate the applicability of our framework by carrying out a few case studies, we provide examples witnessing limitations of our approach, and we discuss general closure properties which follow from our results.
Cite as

Antonio Casares and Pierre Ohlmann. Characterising Memory in Infinite Games. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 122:1-122:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2023.122,
  author =	{Casares, Antonio and Ohlmann, Pierre},
  title =	{{Characterising Memory in Infinite Games}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{122:1--122:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.122},
  URN =		{urn:nbn:de:0030-drops-181740},
  doi =		{10.4230/LIPIcs.ICALP.2023.122},
  annote =	{Keywords: Infinite duration games, Memory, Universal graphs}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.128
Flipper Games for Monadically Stable Graph Classes

Authors: Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokołowski, and Szymon Toruńczyk

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
A class of graphs C is monadically stable if for every unary expansion Ĉ of C, one cannot encode - using first-order transductions - arbitrarily long linear orders in graphs from C. It is known that nowhere dense graph classes are monadically stable; these include classes of bounded maximum degree and classes that exclude a fixed topological minor. On the other hand, monadic stability is a property expressed in purely model-theoretic terms that is also suited for capturing structure in dense graphs. In this work we provide a characterization of monadic stability in terms of the Flipper game: a game on a graph played by Flipper, who in each round can complement the edge relation between any pair of vertex subsets, and Localizer, who in each round is forced to restrict the game to a ball of bounded radius. This is an analog of the Splitter game, which characterizes nowhere dense classes of graphs (Grohe, Kreutzer, and Siebertz, J. ACM '17). We give two different proofs of our main result. The first proof is based on tools borrowed from model theory, and it exposes an additional property of monadically stable graph classes that is close in spirit to definability of types. Also, as a byproduct, we show that monadic stability for graph classes coincides with monadic stability of existential formulas with two free variables, and we provide another combinatorial characterization of monadic stability via forbidden patterns. The second proof relies on the recently introduced notion of flip-flatness (Dreier, Mählmann, Siebertz, and Toruńczyk, arXiv 2206.13765) and provides an efficient algorithm to compute Flipper’s moves in a winning strategy.
Cite as

Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokołowski, and Szymon Toruńczyk. Flipper Games for Monadically Stable Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 128:1-128:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2023.128,
  author =	{Gajarsk\'{y}, Jakub and M\"{a}hlmann, Nikolas and McCarty, Rose and Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Siebertz, Sebastian and Soko{\l}owski, Marek and Toru\'{n}czyk, Szymon},
  title =	{{Flipper Games for Monadically Stable Graph Classes}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{128:1--128:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.128},
  URN =		{urn:nbn:de:0030-drops-181804},
  doi =		{10.4230/LIPIcs.ICALP.2023.128},
  annote =	{Keywords: Stability theory, structural graph theory, games}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.135
Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes

Authors: Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We use model-theoretic tools originating from stability theory to derive a result we call the Finitary Substitute Lemma, which intuitively says the following. Suppose we work in a stable graph class 𝒞, and using a first-order formula φ with parameters we are able to define, in every graph G ∈ 𝒞, a relation R that satisfies some hereditary first-order assertion ψ. Then we are able to find a first-order formula φ' that has the same property, but additionally is finitary: there is finite bound k ∈ ℕ such that in every graph G ∈ 𝒞, different choices of parameters give only at most k different relations R that can be defined using φ'. We use the Finitary Substitute Lemma to derive two corollaries about the existence of certain canonical decompositions in classes of well-structured graphs. - We prove that in the Splitter game, which characterizes nowhere dense graph classes, and in the Flipper game, which characterizes monadically stable graph classes, there is a winning strategy for Splitter, respectively Flipper, that can be defined in first-order logic from the game history. Thus, the strategy is canonical. - We show that for any fixed graph class 𝒞 of bounded shrubdepth, there is an 𝒪(n²)-time algorithm that given an n-vertex graph G ∈ 𝒞, computes in an isomorphism-invariant way a structure H of bounded treedepth in which G can be interpreted. A corollary of this result is an 𝒪(n²)-time isomorphism test and canonization algorithm for any fixed class of bounded shrubdepth.
Cite as

Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 135:1-135:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ohlmann_et_al:LIPIcs.ICALP.2023.135,
  author =	{Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Toru\'{n}czyk, Szymon},
  title =	{{Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{135:1--135:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.135},
  URN =		{urn:nbn:de:0030-drops-181874},
  doi =		{10.4230/LIPIcs.ICALP.2023.135},
  annote =	{Keywords: Model Theory, Stability Theory, Shrubdepth, Nowhere Dense, Monadically Stable}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.44
A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games

Authors: K. S. Thejaswini, Pierre Ohlmann, and Marcin Jurdziński

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
The classic McNaughton-Zielonka algorithm for solving parity games has excellent performance in practice, but its worst-case asymptotic complexity is worse than that of the state-of-the-art algorithms. This work pinpoints the mechanism that is responsible for this relative underperformance and proposes a new technique that eliminates it. The culprit is the wasteful manner in which the results obtained from recursive calls are indiscriminately discarded by the algorithm whenever subgames on which the algorithm is run change. Our new technique is based on firstly enhancing the algorithm to compute attractor decompositions of subgames instead of just winning strategies on them, and then on making it carefully use attractor decompositions computed in prior recursive calls to reduce the size of subgames on which further recursive calls are made. We illustrate the new technique on the classic example of the recursive McNaughton-Zielonka algorithm, but it can be applied to other symmetric attractor-based algorithms that were inspired by it, such as the quasi-polynomial versions of the McNaughton-Zielonka algorithm based on universal trees.
Cite as

K. S. Thejaswini, Pierre Ohlmann, and Marcin Jurdziński. A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 44:1-44:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{thejaswini_et_al:LIPIcs.FSTTCS.2022.44,
  author =	{Thejaswini, K. S. and Ohlmann, Pierre and Jurdzi\'{n}ski, Marcin},
  title =	{{A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{44:1--44:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.44},
  URN =		{urn:nbn:de:0030-drops-174365},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.44},
  annote =	{Keywords: Parity games, Attractor decomposition, Quasipolynomial Algorithms, Universal trees}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.34
Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games

Authors: Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We study the computational complexity of solving mean payoff games. This class of games can be seen as an extension of parity games, and they have similar complexity status: in both cases solving them is in NP ∩ coNP and not known to be in P. In a breakthrough result Calude, Jain, Khoussainov, Li, and Stephan constructed in 2017 a quasipolynomial time algorithm for solving parity games, which was quickly followed by a few other algorithms with the same complexity. Our objective is to investigate how these techniques can be extended to mean payoff games. The starting point is the combinatorial notion of universal trees: all quasipolynomial time algorithms for parity games have been shown to exploit universal trees. Universal graphs extend universal trees to arbitrary (positionally determined) objectives. We show that they yield a family of value iteration algorithms for solving mean payoff games which includes the value iteration algorithm due to Brim, Chaloupka, Doyen, Gentilini, and Raskin. The contribution of this paper is to prove tight bounds on the complexity of algorithms for mean payoff games using universal graphs. We consider two parameters: the largest weight N in absolute value and the number k of weights. The dependence in N in the existing value iteration algorithm is linear, we show that this can be improved to N^{1 - 1/n} and obtain a matching lower bound. However, we show that we cannot break the linear dependence in the exponent in the number k of weights implying that universal graphs do not yield a quasipolynomial time algorithm for solving mean payoff games.
Cite as

Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann. Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.MFCS.2020.34,
  author =	{Fijalkow, Nathana\"{e}l and Gawrychowski, Pawe{\l} and Ohlmann, Pierre},
  title =	{{Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.34},
  URN =		{urn:nbn:de:0030-drops-127011},
  doi =		{10.4230/LIPIcs.MFCS.2020.34},
  annote =	{Keywords: Mean payoff games, Universal graphs, Value iteration}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.24
Lower Bounds for Arithmetic Circuits via the Hankel Matrix

Authors: Nathanaël Fijalkow, Guillaume Lagarde, Pierre Ohlmann, and Olivier Serre

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
We study the complexity of representing polynomials by arithmetic circuits in both the commutative and the non-commutative settings. To analyse circuits we count their number of parse trees, which describe the non-associative computations realised by the circuit. In the non-commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d)} parse trees. Previous superpolynomial lower bounds were known for circuits with up to 2^{d^{1/3-ε}} parse trees, for any ε > 0. Our main result is to reduce the gap by showing a superpolynomial lower bound for circuits with just a small defect in the exponent for the total number of parse trees, that is 2^{d^{1 - ε}}, for any ε > 0. In the commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d log d)} parse trees. We show a superpolynomial lower bound for circuits with up to 2^{d^{1/3 - ε}} parse trees, for any ε > 0. When d is polylogarithmic in n, we push this further to up to 2^{d^{1 - ε}} parse trees. While these two main results hold in the associative setting, our approach goes through a precise understanding of the more restricted setting where multiplication is not associative, meaning that we distinguish the polynomials (xy)z and x(yz). Our first and main conceptual result is a characterization result: we show that the size of the smallest circuit computing a given non-associative polynomial is exactly the rank of a matrix constructed from the polynomial and called the Hankel matrix. This result applies to the class of all circuits in both commutative and non-commutative settings, and can be seen as an extension of the seminal result of Nisan giving a similar characterization for non-commutative algebraic branching programs. Our key technical contribution is to provide generic lower bound theorems based on analyzing and decomposing the Hankel matrix, from which we derive the results mentioned above. The study of the Hankel matrix also provides a unifying approach for proving lower bounds for polynomials in the (classical) associative setting. We demonstrate this by giving alternative proofs of recent lower bounds as corollaries of our generic lower bound results.
Cite as

Nathanaël Fijalkow, Guillaume Lagarde, Pierre Ohlmann, and Olivier Serre. Lower Bounds for Arithmetic Circuits via the Hankel Matrix. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.STACS.2020.24,
  author =	{Fijalkow, Nathana\"{e}l and Lagarde, Guillaume and Ohlmann, Pierre and Serre, Olivier},
  title =	{{Lower Bounds for Arithmetic Circuits via the Hankel Matrix}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.24},
  URN =		{urn:nbn:de:0030-drops-118859},
  doi =		{10.4230/LIPIcs.STACS.2020.24},
  annote =	{Keywords: Arithmetic Circuit Complexity, Lower Bounds, Parse Trees, Hankel Matrix}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.29
Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

Authors: Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
The Orbit Problem consists of determining, given a linear transformation A on d-dimensional rationals Q^d, together with vectors x and y, whether the orbit of x under repeated applications of A can ever reach y. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable invariants P which are subsets of R^d, i.e., sets that are stable under A and contain x and not y, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size. It is worth noting that the existence of semilinear invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.
Cite as

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell. Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.STACS.2017.29,
  author =	{Fijalkow, Nathana\"{e}l and Ohlmann, Pierre and Ouaknine, Jo\"{e}l and Pouly, Amaury and Worrell, James},
  title =	{{Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{29:1--29:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.29},
  URN =		{urn:nbn:de:0030-drops-70059},
  doi =		{10.4230/LIPIcs.STACS.2017.29},
  annote =	{Keywords: Verification,algebraic computation,Skolem Problem,Orbit Problem,invariants}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact